Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
1(1(x1)) → 4(3(x1))
1(2(x1)) → 2(1(x1))
2(2(x1)) → 1(1(1(x1)))
3(3(x1)) → 5(6(x1))
3(4(x1)) → 1(1(x1))
4(4(x1)) → 3(x1)
5(5(x1)) → 6(2(x1))
5(6(x1)) → 1(2(x1))
6(6(x1)) → 2(1(x1))
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
1(1(x1)) → 4(3(x1))
1(2(x1)) → 2(1(x1))
2(2(x1)) → 1(1(1(x1)))
3(3(x1)) → 5(6(x1))
3(4(x1)) → 1(1(x1))
4(4(x1)) → 3(x1)
5(5(x1)) → 6(2(x1))
5(6(x1)) → 1(2(x1))
6(6(x1)) → 2(1(x1))
Q is empty.
We use [27] with the following order to prove termination.
Knuth-Bendix order [24] with precedence:
31 > 11 > 21
31 > 11 > 41
and weight map:
5_1=44731872512
1_1=32471712256
3_1=43247130624
2_1=48725750528
6_1=40598731520
4_1=21696293888
dummyConstant=1